$\forall$${\it Cmd}$:Type, $x$:chain\_sys(${\it Cmd}$). ($\uparrow$csinput?($x$)) $\Rightarrow$ (csinput{-}cmd($x$) $\in$ ${\it Cmd}$)